<?xml version="1.0" encoding="utf-8" ?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml" xml:lang="en" lang="en">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<meta name="generator" content="Docutils 0.11: http://docutils.sourceforge.net/" />
<title>Testing a Simple Program with S2E</title>
<link rel="stylesheet" href="./s2e.css" type="text/css" />
</head>
<body>
<div class="document" id="testing-a-simple-program-with-s2e">
<h1 class="title">Testing a Simple Program with S2E</h1>

<p>This tutorial assumes that you have already built S2E and prepared VM image as described
on the <a class="reference external" href="BuildingS2E.html">Building the S2E Framework</a> page.</p>
<div class="contents topic" id="contents">
<p class="topic-title first">Contents</p>
<ul class="simple">
<li><a class="reference internal" href="#program-to-test" id="id1">Program to Test</a></li>
<li><a class="reference internal" href="#compiling-the-program-in-the-guest" id="id2">Compiling the Program in the Guest</a></li>
<li><a class="reference internal" href="#preparing-the-program-for-s2e" id="id3">Preparing the Program for S2E</a></li>
<li><a class="reference internal" href="#running-the-program-in-s2e" id="id4">Running the Program in S2E</a></li>
<li><a class="reference internal" href="#exploring-the-program-faster" id="id5">Exploring the Program Faster</a></li>
<li><a class="reference internal" href="#minimal-configuration-file" id="id6">Minimal Configuration File</a></li>
</ul>
</div>
<div class="section" id="program-to-test">
<h1>Program to Test</h1>
<p>We want to cover all of the code of the following program by exploring all
the possible paths through it.</p>
<div class="highlight"><pre><span class="cp">#include &lt;stdio.h&gt;</span>
<span class="cp">#include &lt;string.h&gt;</span>

<span class="kt">int</span> <span class="nf">main</span><span class="p">(</span><span class="kt">void</span><span class="p">)</span>
<span class="p">{</span>
  <span class="kt">char</span> <span class="n">str</span><span class="p">[</span><span class="mi">3</span><span class="p">];</span>
  <span class="n">printf</span><span class="p">(</span><span class="s">&quot;Enter two characters: &quot;</span><span class="p">);</span>
  <span class="k">if</span><span class="p">(</span><span class="o">!</span><span class="n">fgets</span><span class="p">(</span><span class="n">str</span><span class="p">,</span> <span class="k">sizeof</span><span class="p">(</span><span class="n">str</span><span class="p">),</span> <span class="n">stdin</span><span class="p">))</span>
    <span class="k">return</span> <span class="mi">1</span><span class="p">;</span>

  <span class="k">if</span><span class="p">(</span><span class="n">str</span><span class="p">[</span><span class="mi">0</span><span class="p">]</span> <span class="o">==</span> <span class="sc">&#39;\n&#39;</span> <span class="o">||</span> <span class="n">str</span><span class="p">[</span><span class="mi">1</span><span class="p">]</span> <span class="o">==</span> <span class="sc">&#39;\n&#39;</span><span class="p">)</span> <span class="p">{</span>
    <span class="n">printf</span><span class="p">(</span><span class="s">&quot;Not enough characters</span><span class="se">\n</span><span class="s">&quot;</span><span class="p">);</span>
  <span class="p">}</span> <span class="k">else</span> <span class="p">{</span>
    <span class="k">if</span><span class="p">(</span><span class="n">str</span><span class="p">[</span><span class="mi">0</span><span class="p">]</span> <span class="o">&gt;=</span> <span class="sc">&#39;a&#39;</span> <span class="o">&amp;&amp;</span> <span class="n">str</span><span class="p">[</span><span class="mi">0</span><span class="p">]</span> <span class="o">&lt;=</span> <span class="sc">&#39;z&#39;</span><span class="p">)</span>
      <span class="n">printf</span><span class="p">(</span><span class="s">&quot;First char is lowercase</span><span class="se">\n</span><span class="s">&quot;</span><span class="p">);</span>
    <span class="k">else</span>
      <span class="n">printf</span><span class="p">(</span><span class="s">&quot;First char is not lowercase</span><span class="se">\n</span><span class="s">&quot;</span><span class="p">);</span>

    <span class="k">if</span><span class="p">(</span><span class="n">str</span><span class="p">[</span><span class="mi">0</span><span class="p">]</span> <span class="o">&gt;=</span> <span class="sc">&#39;0&#39;</span> <span class="o">&amp;&amp;</span> <span class="n">str</span><span class="p">[</span><span class="mi">0</span><span class="p">]</span> <span class="o">&lt;=</span> <span class="sc">&#39;9&#39;</span><span class="p">)</span>
      <span class="n">printf</span><span class="p">(</span><span class="s">&quot;First char is a digit</span><span class="se">\n</span><span class="s">&quot;</span><span class="p">);</span>
    <span class="k">else</span>
      <span class="n">printf</span><span class="p">(</span><span class="s">&quot;First char is not a digit</span><span class="se">\n</span><span class="s">&quot;</span><span class="p">);</span>

    <span class="k">if</span><span class="p">(</span><span class="n">str</span><span class="p">[</span><span class="mi">0</span><span class="p">]</span> <span class="o">==</span> <span class="n">str</span><span class="p">[</span><span class="mi">1</span><span class="p">])</span>
      <span class="n">printf</span><span class="p">(</span><span class="s">&quot;First and second chars are the same</span><span class="se">\n</span><span class="s">&quot;</span><span class="p">);</span>
    <span class="k">else</span>
      <span class="n">printf</span><span class="p">(</span><span class="s">&quot;First and second chars are not the same</span><span class="se">\n</span><span class="s">&quot;</span><span class="p">);</span>
  <span class="p">}</span>

  <span class="k">return</span> <span class="mi">0</span><span class="p">;</span>
<span class="p">}</span>
</pre></div>
</div>
<div class="section" id="compiling-the-program-in-the-guest">
<h1>Compiling the Program in the Guest</h1>
<p>Before testing the program in S2E, compile and run it in the native QEMU build
(the one in the <tt class="docutils literal"><span class="pre">i386-softmmu</span></tt> directory).
Launch QEMU with the following command:</p>
<pre class="literal-block">
$ $S2EDIR/build/i386-softmmu/qemu-system-i386 your_image.raw
</pre>
<p>You need to copy the example source code into the VM. As you will likely need to do this
frequently, we recommend to install either <tt class="docutils literal">ssh</tt> or an http server on your host
machine. Then you can copy the code using <tt class="docutils literal">scp</tt>:</p>
<pre class="literal-block">
guest$ scp &lt;your_login_on_host&gt;&#64;&lt;your_host_name&gt;:path/to/tutorial1.c .
guest$ scp &lt;your_login_on_host&gt;&#64;&lt;your_host_name&gt;:path/to/s2e/guest/include/s2e.h .
</pre>
<p>Compile and run the example with the following commands:</p>
<pre class="literal-block">
guest$ gcc -O3 tutorial1.c -o tutorial1
guest$ ./tutorial1
Enter two characters: ab
First char is lowercase
First char is not a digit
First and second chars are not the same
</pre>
</div>
<div class="section" id="preparing-the-program-for-s2e">
<h1>Preparing the Program for S2E</h1>
<p>In order to execute the program symbolically, it is necessary to specify what
values should become symbolic. There are many ways to do it in S2E, but the
simplest one is to use the S2E opcodes library. This library provides a way for
guest code to communicate with the S2E system.</p>
<p>In order to explore all possible paths through the program that correspond to
all possible inputs, we want to make these inputs symbolic. To accomplish this, we
replace the call to <tt class="docutils literal">fgets()</tt> by a call to <tt class="docutils literal">s2e_make_symbolic()</tt>:</p>
<div class="highlight"><pre><span class="p">...</span>
<span class="kt">char</span> <span class="n">str</span><span class="p">[</span><span class="mi">3</span><span class="p">];</span>
<span class="c1">// printf(&quot;Enter two characters: &quot;);</span>
<span class="c1">// if(!fgets(str, sizeof(str), stdin))</span>
<span class="c1">//   return 1;</span>
<span class="n">s2e_make_symbolic</span><span class="p">(</span><span class="n">str</span><span class="p">,</span> <span class="mi">2</span><span class="p">,</span> <span class="s">&quot;str&quot;</span><span class="p">);</span>
<span class="n">str</span><span class="p">[</span><span class="mi">3</span><span class="p">]</span> <span class="o">=</span> <span class="mi">0</span><span class="p">;</span>
<span class="p">...</span>
</pre></div>
<p>By default, S2E propagates the symbolic values through the program but does
not fork on branches. To enable forking, call
<tt class="docutils literal">s2e_enable_forking()</tt> before making symbolic values, and
<tt class="docutils literal">s2e_disable_forking()</tt> after exploring all branches.</p>
<p>Finally, it would be interesting to see an example of input value that cause a
program to take a particular execution path. This can be useful to reproduce a bug
in a debugger, independently of S2E.
For that, use the <tt class="docutils literal">s2e_get_example()</tt> function. This function gives a concrete example of symbolic values
that satisfy the current path constraints (i.e., all branch conditions along the
execution path).</p>
<p>After these changes, the example program looks as follows:</p>
<div class="highlight"><pre><span class="cp">#include &lt;stdio.h&gt;</span>
<span class="cp">#include &lt;string.h&gt;</span>
<span class="cp">#include &quot;s2e.h&quot;</span>

<span class="kt">int</span> <span class="nf">main</span><span class="p">(</span><span class="kt">void</span><span class="p">)</span>
<span class="p">{</span>
  <span class="kt">char</span> <span class="n">str</span><span class="p">[</span><span class="mi">3</span><span class="p">];</span>
  <span class="c1">// printf(&quot;Enter two characters: &quot;);</span>
  <span class="c1">// if(!fgets(str, sizeof(str), stdin))</span>
  <span class="c1">//   return 1;</span>

  <span class="n">s2e_enable_forking</span><span class="p">();</span>
  <span class="n">s2e_make_symbolic</span><span class="p">(</span><span class="n">str</span><span class="p">,</span> <span class="mi">2</span><span class="p">,</span> <span class="s">&quot;str&quot;</span><span class="p">);</span>

  <span class="k">if</span><span class="p">(</span><span class="n">str</span><span class="p">[</span><span class="mi">0</span><span class="p">]</span> <span class="o">==</span> <span class="sc">&#39;\n&#39;</span> <span class="o">||</span> <span class="n">str</span><span class="p">[</span><span class="mi">1</span><span class="p">]</span> <span class="o">==</span> <span class="sc">&#39;\n&#39;</span><span class="p">)</span> <span class="p">{</span>
    <span class="n">printf</span><span class="p">(</span><span class="s">&quot;Not enough characters</span><span class="se">\n</span><span class="s">&quot;</span><span class="p">);</span>
  <span class="p">}</span> <span class="k">else</span> <span class="p">{</span>
    <span class="k">if</span><span class="p">(</span><span class="n">str</span><span class="p">[</span><span class="mi">0</span><span class="p">]</span> <span class="o">&gt;=</span> <span class="sc">&#39;a&#39;</span> <span class="o">&amp;&amp;</span> <span class="n">str</span><span class="p">[</span><span class="mi">0</span><span class="p">]</span> <span class="o">&lt;=</span> <span class="sc">&#39;z&#39;</span><span class="p">)</span>
      <span class="n">printf</span><span class="p">(</span><span class="s">&quot;First char is lowercase</span><span class="se">\n</span><span class="s">&quot;</span><span class="p">);</span>
    <span class="k">else</span>
      <span class="n">printf</span><span class="p">(</span><span class="s">&quot;First char is not lowercase</span><span class="se">\n</span><span class="s">&quot;</span><span class="p">);</span>

    <span class="k">if</span><span class="p">(</span><span class="n">str</span><span class="p">[</span><span class="mi">0</span><span class="p">]</span> <span class="o">&gt;=</span> <span class="sc">&#39;0&#39;</span> <span class="o">&amp;&amp;</span> <span class="n">str</span><span class="p">[</span><span class="mi">0</span><span class="p">]</span> <span class="o">&lt;=</span> <span class="sc">&#39;9&#39;</span><span class="p">)</span>
      <span class="n">printf</span><span class="p">(</span><span class="s">&quot;First char is a digit</span><span class="se">\n</span><span class="s">&quot;</span><span class="p">);</span>
    <span class="k">else</span>
      <span class="n">printf</span><span class="p">(</span><span class="s">&quot;First char is not a digit</span><span class="se">\n</span><span class="s">&quot;</span><span class="p">);</span>

    <span class="k">if</span><span class="p">(</span><span class="n">str</span><span class="p">[</span><span class="mi">0</span><span class="p">]</span> <span class="o">==</span> <span class="n">str</span><span class="p">[</span><span class="mi">1</span><span class="p">])</span>
      <span class="n">printf</span><span class="p">(</span><span class="s">&quot;First and second chars are the same</span><span class="se">\n</span><span class="s">&quot;</span><span class="p">);</span>
    <span class="k">else</span>
      <span class="n">printf</span><span class="p">(</span><span class="s">&quot;First and second chars are not the same</span><span class="se">\n</span><span class="s">&quot;</span><span class="p">);</span>
  <span class="p">}</span>

  <span class="n">s2e_disable_forking</span><span class="p">();</span>

  <span class="n">s2e_get_example</span><span class="p">(</span><span class="n">str</span><span class="p">,</span> <span class="mi">2</span><span class="p">);</span>
  <span class="n">printf</span><span class="p">(</span><span class="s">&quot;&#39;%c%c&#39; %02x %02x</span><span class="se">\n</span><span class="s">&quot;</span><span class="p">,</span> <span class="n">str</span><span class="p">[</span><span class="mi">0</span><span class="p">],</span> <span class="n">str</span><span class="p">[</span><span class="mi">1</span><span class="p">],</span>
         <span class="p">(</span><span class="kt">unsigned</span> <span class="kt">char</span><span class="p">)</span> <span class="n">str</span><span class="p">[</span><span class="mi">0</span><span class="p">],</span> <span class="p">(</span><span class="kt">unsigned</span> <span class="kt">char</span><span class="p">)</span> <span class="n">str</span><span class="p">[</span><span class="mi">1</span><span class="p">]);</span>

  <span class="k">return</span> <span class="mi">0</span><span class="p">;</span>
<span class="p">}</span>
</pre></div>
<p>Compile and run the program as usual:</p>
<pre class="literal-block">
guest$ gcc -O3 tutorial1.c -o tutorial1
guest$ ./tutorial1
Illegal instruction
</pre>
<p>You see the <tt class="docutils literal">Illegal instruction</tt> message because all <tt class="docutils literal">s2e_*</tt> functions use
special CPU opcodes that are only recognized by S2E.</p>
</div>
<div class="section" id="running-the-program-in-s2e">
<h1>Running the Program in S2E</h1>
<p>To run a program in S2E, we have to write a configuration file, then reboot
the system in S2E.</p>
<div class="highlight"><pre><span class="c1">-- File: config.lua</span>
<span class="n">s2e</span> <span class="o">=</span> <span class="p">{</span>
  <span class="n">kleeArgs</span> <span class="o">=</span> <span class="p">{</span>
    <span class="c1">-- Pick a random path to execute among all the</span>
    <span class="c1">-- available paths.</span>
    <span class="s2">&quot;</span><span class="s">--use-random-path=true&quot;</span><span class="p">,</span>

    <span class="c1">-- Run each state for at least 1 second before</span>
    <span class="c1">-- switching to the other:</span>
    <span class="s2">&quot;</span><span class="s">--use-batching-search=true&quot;</span><span class="p">,</span> <span class="s2">&quot;</span><span class="s">--batch-time=1.0&quot;</span>
  <span class="p">}</span>
<span class="p">}</span>
<span class="n">plugins</span> <span class="o">=</span> <span class="p">{</span>
  <span class="c1">-- Enable a plugin that handles S2E custom opcode</span>
  <span class="s2">&quot;</span><span class="s">BaseInstructions&quot;</span>
<span class="p">}</span>
</pre></div>
<p><strong>Note:</strong> At the end of this tutorial, there is a section that shows an even simpler
configuration file.</p>
<p>Booting the system in S2E takes a long time. Use a two-step process to
speed it up. First, boot the system in the version of QEMU that has S2E
disabled. Then, save a snapshot and load it in the S2E:</p>
<pre class="literal-block">
guest$ su -c halt # shut down qemu

$ $S2EDIR/build/qemu-release/i386-softmmu/qemu-system-i386 -net none your_image.raw.s2e
&gt; Wait until Linux is loaded, login into the system. Then press
&gt; Ctrl + Alt + 2 and type 'savevm 1' then 'quit'.
&gt; Notice that we use i386-softmmu, which is the build with S2E **disabled**.

$ $S2EDIR/build/qemu-release/i386-s2e-softmmu/qemu-system-i386 -net none your_image.raw.s2e -loadvm 1 \
                           -s2e-config-file config.lua -s2e-verbose
&gt; Wait until the snapshot is resumed, then type in the guest
guest$ ./tutorial1
&gt; Notice that we use i386-s2e-softmmu, which is the build with S2E ENABLED.
</pre>
<p>After you run this command, S2E starts to symbolically execute the example.
The configuration file instructs S2E to pick a random state once per second.
You will see the QEMU screen content changing every
second for different possible outputs of the example.</p>
<p>Each state is a completely independent snapshot of the whole system. You can
even interact with each state independently, for example by launching
different programs. Try to launch <tt class="docutils literal">tutorial1</tt> in one of the states again!</p>
<p>In the host terminal (i.e., the S2E standard output), you see various
information about state execution, forking and switching. This output is
also saved into the <tt class="docutils literal"><span class="pre">s2e-last/messages.txt</span></tt> log file. As an exercise, try to follow the
execution history of a state through the log file.</p>
</div>
<div class="section" id="exploring-the-program-faster">
<h1>Exploring the Program Faster</h1>
<p>In the previous section, we made the program run along multiple execution
paths.  However, each path continued to run even after the program terminated,
executing operating system code.  This is great to visually experience how
S2E works, but in general we want S2E to stop executing each path as soon as
the program to analyze terminates.</p>
<p>Terminating an execution path is accomplished with the <tt class="docutils literal">s2e_kill_state()</tt> function.
A call to this function immediately stops executing the
current state and exits S2E if there are no more states to
explore. Add a call to this function just before the program returns
control to the OS. Before that, we might want to print example values in the
S2E log using <tt class="docutils literal">s2e_message()</tt> or <tt class="docutils literal">s2e_warning()</tt> functions:</p>
<div class="highlight"><pre><span class="kt">int</span> <span class="nf">main</span><span class="p">(</span><span class="kt">void</span><span class="p">)</span>
<span class="p">{</span>
  <span class="kt">char</span> <span class="n">buf</span><span class="p">[</span><span class="mi">32</span><span class="p">];</span>
  <span class="n">memset</span><span class="p">(</span><span class="n">buf</span><span class="p">,</span> <span class="mi">0</span><span class="p">,</span> <span class="k">sizeof</span><span class="p">(</span><span class="n">buf</span><span class="p">));</span>
  <span class="p">...</span>

  <span class="p">...</span>
  <span class="n">s2e_get_example</span><span class="p">(</span><span class="n">str</span><span class="p">,</span> <span class="mi">2</span><span class="p">);</span>
  <span class="n">snprintf</span><span class="p">(</span><span class="n">buf</span><span class="p">,</span> <span class="k">sizeof</span><span class="p">(</span><span class="n">buf</span><span class="p">),</span> <span class="s">&quot;&#39;%c%c&#39; %02x %02x</span><span class="se">\n</span><span class="s">&quot;</span><span class="p">,</span> <span class="n">str</span><span class="p">[</span><span class="mi">0</span><span class="p">],</span> <span class="n">str</span><span class="p">[</span><span class="mi">1</span><span class="p">],</span>
         <span class="p">(</span><span class="kt">unsigned</span> <span class="kt">char</span><span class="p">)</span> <span class="n">str</span><span class="p">[</span><span class="mi">0</span><span class="p">],</span> <span class="p">(</span><span class="kt">unsigned</span> <span class="kt">char</span><span class="p">)</span> <span class="n">str</span><span class="p">[</span><span class="mi">1</span><span class="p">]);</span>
  <span class="n">s2e_warning</span><span class="p">(</span><span class="n">buf</span><span class="p">);</span>

  <span class="n">s2e_kill_state</span><span class="p">(</span><span class="mi">0</span><span class="p">,</span> <span class="s">&quot;program terminated&quot;</span><span class="p">);</span>

  <span class="k">return</span> <span class="mi">0</span><span class="p">;</span>
<span class="p">}</span>
</pre></div>
<p>Now, resume the snapshot in QEMU with S2E disabled, edit and recompile
the program, re-save the snapshot and re-load it in S2E.
Your image needs to be in <a class="reference external" href="ImageInstallation.html">S2E format</a>.</p>
<pre class="literal-block">
$ $S2EDIR/build/qemu-release/i386-softmmu/qemu-system-i386 -net none your_image.raw.s2e -loadvm 1
guest$ edit tutorial1.c
guest$ gcc -O3 tutorial1.c -o tutorial1
&gt; press Ctrl + Alt + 2 and type 'savevm 1' then type 'quit'.

$ $S2EDIR/build/qemu/i386-s2e-softmmu/qemu-system-i386 -net none your_image.raw.s2e -loadvm 1 \
                           -s2e-config-file config.lua -s2e-verbose
guest$ ./tutorial1
</pre>
<p>Running <tt class="docutils literal">tutorial1</tt> this time  will make S2E quickly terminate, leaving
a log file that you can examine.</p>
<p>Please note that in case your program crashes or exits at some other point
without calling <tt class="docutils literal">s2e_kill_state()</tt>, S2E will not terminate and will continue to
execute paths that returned to the system. To avoid this, you can use the <tt class="docutils literal">s2ecmd</tt> utility (in <tt class="docutils literal">$S2EDIR/guest</tt>).
Launch it right after the invocation to the program that can crash, e.g., as follows:</p>
<pre class="literal-block">
guest$ ./tutorial; ./s2ecmd kill 0 &quot;done&quot;
</pre>
</div>
<div class="section" id="minimal-configuration-file">
<h1>Minimal Configuration File</h1>
<p>The following is a minimal configuration file that you can use to run this example:</p>
<div class="highlight"><pre><span class="c1">-- File: config.lua</span>
<span class="n">s2e</span> <span class="o">=</span> <span class="p">{</span>
  <span class="n">kleeArgs</span> <span class="o">=</span> <span class="p">{}</span>
<span class="p">}</span>

<span class="n">plugins</span> <span class="o">=</span> <span class="p">{</span>
  <span class="c1">-- Enable a plugin that handles S2E custom opcode</span>
  <span class="s2">&quot;</span><span class="s">BaseInstructions&quot;</span>
<span class="p">}</span>
</pre></div>
<p>In this case S2E uses the default <strong>depth-first searcher (DFS)</strong>.
The current state will run until it is explicitely killed. After that,
S2E will select another path, according to the DFS strategy.
You <strong>must</strong> use <tt class="docutils literal">s2ecmd</tt> or <tt class="docutils literal">s2e_kill_state()</tt>, otherwise the current path will run forever
and there will not be any progress.</p>
</div>
</div>
<div class="footer">
<hr class="footer" />
<a class="reference external" href="TestingMinimalProgram.rst">View document source</a>.

</div>
</body>
</html>
